Skip to content

Aslp generating control flow branches#188

Merged
katrinafyi merged 28 commits into
mainfrom
aslp-branches-2
Jun 23, 2026
Merged

Aslp generating control flow branches#188
katrinafyi merged 28 commits into
mainfrom
aslp-branches-2

Conversation

@katrinafyi

@katrinafyi katrinafyi commented Jun 22, 2026

Copy link
Copy Markdown
Collaborator

ensures a pc increment on all straight-line control-flow paths by construction.

adds a new lib/transforms/aslp/aslp_lexpr.ml file for abstracting the builtin and local variables used by the aslp lifter.

this pr also renames some things, like now using aslp_diamond in place of aslp_state.

let%expect_test "lift: b.eq #1024" =
  let module I = (val Bincaml_ibi.from_generator (Aslp_state.empty_aslp_ids ()))
  in
  let x =
    lift_opcode
      (module I)
      ~address:(Bitvec.zero ~size:64)
      (Bitvec.of_string "0x54002000:bv32")
  in
  print_endline @@ Aslp_state.show_aslp_diamond x;
  [%expect
    {|
    { Aslp_state.blocks = "block_0"
      -> { Aslp_state.assume = None; stmts = []; succs = ["block_1"; "block_2"];
           has_pc_assign = false },
      "block_1"
      -> { Aslp_state.assume = (Some eq($PSTATE_Z, 0x1:bv1));
           stmts = [var BranchTaken:bool := true; $PC:bv64 := 0x400:bv64];
           succs = ["block_3"]; has_pc_assign = true },
      "block_2"
      -> { Aslp_state.assume = (Some boolnot(eq($PSTATE_Z, 0x1:bv1)));
           stmts =
           [($PC:bv64 := bvadd($PC, 0x4:bv32), var BranchTaken:bool := false)];
           succs = ["block_3"]; has_pc_assign = true },
      "block_3"
      -> { Aslp_state.assume = None; stmts = []; succs = []; has_pc_assign = true
           };
      entry = "block_0"; exit = "block_3" }
    |}]

@katrinafyi katrinafyi requested a review from agle as a code owner June 22, 2026 08:46
@agle agle removed their request for review June 23, 2026 05:32
|> Aslp_state.add_block ~pred:st.active ~name:f ~assume:ncond
|> Aslp_state.add_block ~pred:t ~name:m
|> Aslp_state.add_goto ~source:f ~target:m
|> Aslp_state.modify_block ~name:m ~f:(fun b ->

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Put the Aslp_state local open outside of the sequence of maps :)

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

:'(

@katrinafyi katrinafyi requested a review from agle June 23, 2026 05:38
Comment thread lib/transforms/aslp/aslp_state.ml Outdated
let gen_block_id = gen_block_id
let gen_local_id = gen_local_id
let block_id = ID.name % ID.fresh ~name:"block" block_ids
and local_id = ID.name % ID.fresh ~name:"var" local_ids in

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I always prefer ID.fresh ~name:"var" local_ids %> ID.name

|> Aslp_state.add_block ~pred:st.active ~name:f ~assume:ncond
|> Aslp_state.add_block ~pred:t ~name:m
|> Aslp_state.add_goto ~source:f ~target:m
|> Aslp_state.modify_block ~name:m ~f:(fun b ->

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

:'(

This is used to maintain the invariant that at every control flow point, the
[PC] variable is either assigned on all paths or assigned on no paths (from
the beginning of the instruction). *)
let ensure_pc_consistency state ~left ~right ~join =

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mention guarantee from lifter that it won't assign PC twice.

@katrinafyi katrinafyi enabled auto-merge (squash) June 23, 2026 06:33
@katrinafyi katrinafyi merged commit f2a9e3f into main Jun 23, 2026
9 checks passed
@katrinafyi katrinafyi deleted the aslp-branches-2 branch June 23, 2026 06:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants